<HTML>
<HEAD><TITLE>The dddmp package: files</TITLE></HEAD>
<BODY>

<DL>
 <DT> <A HREF="#dddmp.h"><CODE>dddmp.h</CODE></A>
 <DD> External header file
 <DT> <A HREF="#dddmpInt.h"><CODE>dddmpInt.h</CODE></A>
 <DD> Internal header file
 <DT> <A HREF="#dddmpBinary.c"><CODE>dddmpBinary.c</CODE></A>
 <DD> Input and output BDD codes and integers from/to file
 <DT> <A HREF="#dddmpConvert.c"><CODE>dddmpConvert.c</CODE></A>
 <DD> Conversion between ASCII and binary formats
 <DT> <A HREF="#dddmpDbg.c"><CODE>dddmpDbg.c</CODE></A>
 <DD> Functions to display BDD files
 <DT> <A HREF="#dddmpDdNodeBdd.c"><CODE>dddmpDdNodeBdd.c</CODE></A>
 <DD> Functions to handle BDD node infos and numbering
 <DT> <A HREF="#dddmpDdNodeCnf.c"><CODE>dddmpDdNodeCnf.c</CODE></A>
 <DD> Functions to handle BDD node infos and numbering
    while storing a CNF formula from a BDD or an array of BDDs
 <DT> <A HREF="#dddmpLoad.c"><CODE>dddmpLoad.c</CODE></A>
 <DD> Functions to read in bdds to file
 <DT> <A HREF="#dddmpLoadCnf.c"><CODE>dddmpLoadCnf.c</CODE></A>
 <DD> Functions to read in CNF from file as BDDs.
 <DT> <A HREF="#dddmpNodeAdd.c"><CODE>dddmpNodeAdd.c</CODE></A>
 <DD> Functions to handle ADD node infos and numbering
 <DT> <A HREF="#dddmpNodeBdd.c"><CODE>dddmpNodeBdd.c</CODE></A>
 <DD> Functions to handle BDD node infos and numbering
 <DT> <A HREF="#dddmpNodeCnf.c"><CODE>dddmpNodeCnf.c</CODE></A>
 <DD> Functions to handle BDD node infos and numbering
    while storing a CNF formula from a BDD or an array of BDDs
 <DT> <A HREF="#dddmpStoreAdd.c"><CODE>dddmpStoreAdd.c</CODE></A>
 <DD> Functions to write ADDs to file.
 <DT> <A HREF="#dddmpStoreBdd.c"><CODE>dddmpStoreBdd.c</CODE></A>
 <DD> Functions to write BDDs to file.
 <DT> <A HREF="#dddmpStoreCnf.c"><CODE>dddmpStoreCnf.c</CODE></A>
 <DD> Functions to write out BDDs to file in a CNF format
 <DT> <A HREF="#dddmpStoreMisc.c"><CODE>dddmpStoreMisc.c</CODE></A>
 <DD> Functions to write out bdds to file in prefixed
    and in Blif form.
 <DT> <A HREF="#dddmpUtil.c"><CODE>dddmpUtil.c</CODE></A>
 <DD> Util Functions for the dddmp package
</DL><HR>
<A NAME="dddmp.h"><H1>dddmp.h</H1></A>
External header file <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
 <DD> Checks for fatal bugs

 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
 <DD> Checks for Warnings: If expr==1 it prints out the warning
    on stderr.

 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
 <DD> Checks for fatal bugs and return the DDDMP_FAILURE flag.

 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
 <DD> Checks for fatal bugs and go to the label to deal with
    the error.

</DL>
<HR>
<A NAME="dddmpInt.h"><H1>dddmpInt.h</H1></A>
Internal header file <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
 <DD> Memory Allocation Macro for DDDMP

 <DT> <A HREF="dddmpAllDet.html#" TARGET="MAIN"><CODE>()</CODE></A>
 <DD> Memory Free Macro for DDDMP

</DL>
<HR>
<A NAME="dddmpBinary.c"><H1>dddmpBinary.c</H1></A>
Input and output BDD codes and integers from/to file <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Input and output BDD codes and integers from/to file
    in binary mode.
    DD node codes are written as one byte.
    Integers of any length are written as sequences of "linked" bytes.
    For each byte 7 bits are used for data and one (MSBit) as link with
    a further byte (MSB = 1 means one more byte).
    Low level read/write of bytes filter <CR>, <LF> and <ctrl-Z>
    with escape sequences. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#DddmpWriteCode" TARGET="MAIN"><CODE>DddmpWriteCode()</CODE></A>
 <DD> Writes 1 byte node code

 <DT> <A HREF="dddmpAllDet.html#DddmpReadCode" TARGET="MAIN"><CODE>DddmpReadCode()</CODE></A>
 <DD> Reads a 1 byte node code

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteInt" TARGET="MAIN"><CODE>DddmpWriteInt()</CODE></A>
 <DD> Writes a "packed integer"

 <DT> <A HREF="dddmpAllDet.html#DddmpReadInt" TARGET="MAIN"><CODE>DddmpReadInt()</CODE></A>
 <DD> Reads a "packed integer"

 <DT> <A HREF="dddmpAllDet.html#WriteByteBinary" TARGET="MAIN"><CODE>WriteByteBinary()</CODE></A>
 <DD> Writes a byte to file filtering <CR>, <LF> and <ctrl-Z>

 <DT> <A HREF="dddmpAllDet.html#ReadByteBinary" TARGET="MAIN"><CODE>ReadByteBinary()</CODE></A>
 <DD> Reads a byte from file with escaped <CR>, <LF> and <ctrl-Z>

</DL>
<HR>
<A NAME="dddmpConvert.c"><H1>dddmpConvert.c</H1></A>
Conversion between ASCII and binary formats <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Conversion between ASCII and binary formats is presently 
    supported by loading a BDD in the source format and storing it 
    in the target one. We plan to introduce ad hoc procedures
    avoiding explicit BDD node generation. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_Text2Bin" TARGET="MAIN"><CODE>Dddmp_Text2Bin()</CODE></A>
 <DD> Converts from ASCII to binary format

 <DT> <A HREF="dddmpAllDet.html#Dddmp_Bin2Text" TARGET="MAIN"><CODE>Dddmp_Bin2Text()</CODE></A>
 <DD> Converts from binary to ASCII format

</DL>
<HR>
<A NAME="dddmpDbg.c"><H1>dddmpDbg.c</H1></A>
Functions to display BDD files <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to display BDD files in binary format <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddDisplayBinary" TARGET="MAIN"><CODE>Dddmp_cuddBddDisplayBinary()</CODE></A>
 <DD> Display a binary dump file in a text file

</DL>
<HR>
<A NAME="dddmpDdNodeBdd.c"><H1>dddmpDdNodeBdd.c</H1></A>
Functions to handle BDD node infos and numbering <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to handle BDD node infos and numbering. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#DddmpNumberDdNodes" TARGET="MAIN"><CODE>DddmpNumberDdNodes()</CODE></A>
 <DD> Removes nodes from unique table and number them

 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberDdNodes" TARGET="MAIN"><CODE>DddmpUnnumberDdNodes()</CODE></A>
 <DD> Restores nodes in unique table, loosing numbering

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndex" TARGET="MAIN"><CODE>DddmpWriteNodeIndex()</CODE></A>
 <DD> Write index to node

 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndex" TARGET="MAIN"><CODE>DddmpReadNodeIndex()</CODE></A>
 <DD> Reads the index of a node

 <DT> <A HREF="dddmpAllDet.html#DddmpVisited" TARGET="MAIN"><CODE>DddmpVisited()</CODE></A>
 <DD> Returns true if node is visited

 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisited" TARGET="MAIN"><CODE>DddmpSetVisited()</CODE></A>
 <DD> Marks a node as visited

 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisited" TARGET="MAIN"><CODE>DddmpClearVisited()</CODE></A>
 <DD> Marks a node as not visited

 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecur" TARGET="MAIN"><CODE>NumberNodeRecur()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecur" TARGET="MAIN"><CODE>RemoveFromUniqueRecur()</CODE></A>
 <DD> Removes a node from unique table

 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecur" TARGET="MAIN"><CODE>RestoreInUniqueRecur()</CODE></A>
 <DD> Restores a node in unique table

</DL>
<HR>
<A NAME="dddmpDdNodeCnf.c"><H1>dddmpDdNodeCnf.c</H1></A>
Functions to handle BDD node infos and numbering
    while storing a CNF formula from a BDD or an array of BDDs <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to handle BDD node infos and numbering
    while storing a CNF formula from a BDD or an array of BDDs. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#DddmpNumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpNumberDdNodesCnf()</CODE></A>
 <DD> Removes nodes from unique table and numbers them

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesAndNumber" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesAndNumber()</CODE></A>
 <DD> Removes nodes from unique table and numbers each node according
    to the number of its incoming BDD edges.

 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpUnnumberDdNodesCnf()</CODE></A>
 <DD> Restores nodes in unique table, loosing numbering

 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNext" TARGET="MAIN"><CODE>DddmpPrintBddAndNext()</CODE></A>
 <DD> Prints debug information

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnfBis" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnfBis()</CODE></A>
 <DD> Write index to node

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnf" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnf()</CODE></A>
 <DD> Write index to node

 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexCnf" TARGET="MAIN"><CODE>DddmpReadNodeIndexCnf()</CODE></A>
 <DD> Reads the index of a node

 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnfRecur" TARGET="MAIN"><CODE>DddmpClearVisitedCnfRecur()</CODE></A>
 <DD> Mark ALL nodes as not visited

 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedCnf" TARGET="MAIN"><CODE>DddmpVisitedCnf()</CODE></A>
 <DD> Returns true if node is visited

 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedCnf" TARGET="MAIN"><CODE>DddmpSetVisitedCnf()</CODE></A>
 <DD> Marks a node as visited

 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnf" TARGET="MAIN"><CODE>DddmpClearVisitedCnf()</CODE></A>
 <DD> Marks a node as not visited

 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurCnf" TARGET="MAIN"><CODE>NumberNodeRecurCnf()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCheckIncomingAndScanPath" TARGET="MAIN"><CODE>DddmpDdNodesCheckIncomingAndScanPath()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesNumberEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesNumberEdgesRecur()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesResetCountRecur" TARGET="MAIN"><CODE>DddmpDdNodesResetCountRecur()</CODE></A>
 <DD> Resets counter and visited flag for ALL nodes of a BDD

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesRecur()</CODE></A>
 <DD> Counts the number of incoming edges for each node of a BDD

 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurCnf" TARGET="MAIN"><CODE>RemoveFromUniqueRecurCnf()</CODE></A>
 <DD> Removes a node from unique table

 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurCnf" TARGET="MAIN"><CODE>RestoreInUniqueRecurCnf()</CODE></A>
 <DD> Restores a node in unique table

 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNextRecur" TARGET="MAIN"><CODE>DddmpPrintBddAndNextRecur()</CODE></A>
 <DD> Prints debug info

</DL>
<HR>
<A NAME="dddmpLoad.c"><H1>dddmpLoad.c</H1></A>
Functions to read in bdds to file <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to read in bdds to file.  BDDs
    are represended on file either in text or binary format under the
    following rules.  A file contains a forest of BDDs (a vector of
    Boolean functions).  BDD nodes are numbered with contiguous numbers,
    from 1 to NNodes (total number of nodes on a file). 0 is not used to
    allow negative node indexes for complemented edges.  A file contains
    a header, including information about variables and roots to BDD
    functions, followed by the list of nodes.  BDD nodes are listed
    according to their numbering, and in the present implementation
    numbering follows a post-order strategy, in such a way that a node
    is never listed before its Then/Else children. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddLoad" TARGET="MAIN"><CODE>Dddmp_cuddBddLoad()</CODE></A>
 <DD> Reads a dump file representing the argument BDD.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayLoad" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayLoad()</CODE></A>
 <DD> Reads a dump file representing the argument BDDs.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddLoad" TARGET="MAIN"><CODE>Dddmp_cuddAddLoad()</CODE></A>
 <DD> Reads a dump file representing the argument ADD.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddArrayLoad" TARGET="MAIN"><CODE>Dddmp_cuddAddArrayLoad()</CODE></A>
 <DD> Reads a dump file representing the argument ADDs.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddHeaderLoad" TARGET="MAIN"><CODE>Dddmp_cuddHeaderLoad()</CODE></A>
 <DD> Reads the header of a dump file representing the argument BDDs

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayLoad" TARGET="MAIN"><CODE>DddmpCuddDdArrayLoad()</CODE></A>
 <DD> Reads a dump file representing the argument BDDs.

 <DT> <A HREF="dddmpAllDet.html#DddmpBddReadHeader" TARGET="MAIN"><CODE>DddmpBddReadHeader()</CODE></A>
 <DD> Reads a the header of a dump file representing the
    argument BDDs.

 <DT> <A HREF="dddmpAllDet.html#DddmpFreeHeader" TARGET="MAIN"><CODE>DddmpFreeHeader()</CODE></A>
 <DD> Frees the internal header structure.

</DL>
<HR>
<A NAME="dddmpLoadCnf.c"><H1>dddmpLoadCnf.c</H1></A>
Functions to read in CNF from file as BDDs. <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to read in CNF from file as BDDs. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddLoadCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddLoadCnf()</CODE></A>
 <DD> Reads a dump file in a CNF format.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayLoadCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayLoadCnf()</CODE></A>
 <DD> Reads a dump file in a CNF format.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddHeaderLoadCnf" TARGET="MAIN"><CODE>Dddmp_cuddHeaderLoadCnf()</CODE></A>
 <DD> Reads the header of a dump file representing the argument BDDs

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayLoadCnf" TARGET="MAIN"><CODE>DddmpCuddDdArrayLoadCnf()</CODE></A>
 <DD> Reads a dump file representing the argument BDDs in CNF
     format.

 <DT> <A HREF="dddmpAllDet.html#DddmpBddReadHeaderCnf" TARGET="MAIN"><CODE>DddmpBddReadHeaderCnf()</CODE></A>
 <DD> Reads a the header of a dump file representing the argument 
    BDDs.

 <DT> <A HREF="dddmpAllDet.html#DddmpFreeHeaderCnf" TARGET="MAIN"><CODE>DddmpFreeHeaderCnf()</CODE></A>
 <DD> Frees the internal header structure.

 <DT> <A HREF="dddmpAllDet.html#DddmpReadCnfClauses" TARGET="MAIN"><CODE>DddmpReadCnfClauses()</CODE></A>
 <DD> Read the CNF clauses from the file in the standard DIMACS
    format.

 <DT> <A HREF="dddmpAllDet.html#DddmpCnfClauses2Bdd" TARGET="MAIN"><CODE>DddmpCnfClauses2Bdd()</CODE></A>
 <DD> Transforms CNF clauses into BDDs.

</DL>
<HR>
<A NAME="dddmpNodeAdd.c"><H1>dddmpNodeAdd.c</H1></A>
Functions to handle ADD node infos and numbering <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to handle ADD node infos and numbering. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#DddmpNumberAddNodes" TARGET="MAIN"><CODE>DddmpNumberAddNodes()</CODE></A>
 <DD> Removes nodes from unique table and number them

 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberAddNodes" TARGET="MAIN"><CODE>DddmpUnnumberAddNodes()</CODE></A>
 <DD> Restores nodes in unique table, loosing numbering

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexAdd" TARGET="MAIN"><CODE>DddmpWriteNodeIndexAdd()</CODE></A>
 <DD> Write index to node

 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexAdd" TARGET="MAIN"><CODE>DddmpReadNodeIndexAdd()</CODE></A>
 <DD> Reads the index of a node

 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedAdd" TARGET="MAIN"><CODE>DddmpVisitedAdd()</CODE></A>
 <DD> Returns true if node is visited

 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedAdd" TARGET="MAIN"><CODE>DddmpSetVisitedAdd()</CODE></A>
 <DD> Marks a node as visited

 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedAdd" TARGET="MAIN"><CODE>DddmpClearVisitedAdd()</CODE></A>
 <DD> Marks a node as not visited

 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurAdd" TARGET="MAIN"><CODE>NumberNodeRecurAdd()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurAdd" TARGET="MAIN"><CODE>RemoveFromUniqueRecurAdd()</CODE></A>
 <DD> Removes a node from unique table

 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurAdd" TARGET="MAIN"><CODE>RestoreInUniqueRecurAdd()</CODE></A>
 <DD> Restores a node in unique table

</DL>
<HR>
<A NAME="dddmpNodeBdd.c"><H1>dddmpNodeBdd.c</H1></A>
Functions to handle BDD node infos and numbering <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to handle BDD node infos and numbering. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#DddmpNumberBddNodes" TARGET="MAIN"><CODE>DddmpNumberBddNodes()</CODE></A>
 <DD> Removes nodes from unique table and number them

 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberBddNodes" TARGET="MAIN"><CODE>DddmpUnnumberBddNodes()</CODE></A>
 <DD> Restores nodes in unique table, loosing numbering

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexBdd" TARGET="MAIN"><CODE>DddmpWriteNodeIndexBdd()</CODE></A>
 <DD> Write index to node

 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexBdd" TARGET="MAIN"><CODE>DddmpReadNodeIndexBdd()</CODE></A>
 <DD> Reads the index of a node

 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedBdd" TARGET="MAIN"><CODE>DddmpVisitedBdd()</CODE></A>
 <DD> Returns true if node is visited

 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedBdd" TARGET="MAIN"><CODE>DddmpSetVisitedBdd()</CODE></A>
 <DD> Marks a node as visited

 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedBdd" TARGET="MAIN"><CODE>DddmpClearVisitedBdd()</CODE></A>
 <DD> Marks a node as not visited

 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurBdd" TARGET="MAIN"><CODE>NumberNodeRecurBdd()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurBdd" TARGET="MAIN"><CODE>RemoveFromUniqueRecurBdd()</CODE></A>
 <DD> Removes a node from unique table

 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurBdd" TARGET="MAIN"><CODE>RestoreInUniqueRecurBdd()</CODE></A>
 <DD> Restores a node in unique table

</DL>
<HR>
<A NAME="dddmpNodeCnf.c"><H1>dddmpNodeCnf.c</H1></A>
Functions to handle BDD node infos and numbering
    while storing a CNF formula from a BDD or an array of BDDs <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to handle BDD node infos and numbering
    while storing a CNF formula from a BDD or an array of BDDs. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#DddmpNumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpNumberDdNodesCnf()</CODE></A>
 <DD> Removes nodes from unique table and numbers them

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesAndNumber" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesAndNumber()</CODE></A>
 <DD> Removes nodes from unique table and numbers each node according
    to the number of its incoming BDD edges.

 <DT> <A HREF="dddmpAllDet.html#DddmpUnnumberDdNodesCnf" TARGET="MAIN"><CODE>DddmpUnnumberDdNodesCnf()</CODE></A>
 <DD> Restores nodes in unique table, loosing numbering

 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNext" TARGET="MAIN"><CODE>DddmpPrintBddAndNext()</CODE></A>
 <DD> Prints debug information

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnf" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnf()</CODE></A>
 <DD> Write index to node

 <DT> <A HREF="dddmpAllDet.html#DddmpVisitedCnf" TARGET="MAIN"><CODE>DddmpVisitedCnf()</CODE></A>
 <DD> Returns true if node is visited

 <DT> <A HREF="dddmpAllDet.html#DddmpSetVisitedCnf" TARGET="MAIN"><CODE>DddmpSetVisitedCnf()</CODE></A>
 <DD> Marks a node as visited

 <DT> <A HREF="dddmpAllDet.html#DddmpReadNodeIndexCnf" TARGET="MAIN"><CODE>DddmpReadNodeIndexCnf()</CODE></A>
 <DD> Reads the index of a node

 <DT> <A HREF="dddmpAllDet.html#DddmpWriteNodeIndexCnfWithTerminalCheck" TARGET="MAIN"><CODE>DddmpWriteNodeIndexCnfWithTerminalCheck()</CODE></A>
 <DD> Write index to node

 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnfRecur" TARGET="MAIN"><CODE>DddmpClearVisitedCnfRecur()</CODE></A>
 <DD> Mark ALL nodes as not visited

 <DT> <A HREF="dddmpAllDet.html#DddmpClearVisitedCnf" TARGET="MAIN"><CODE>DddmpClearVisitedCnf()</CODE></A>
 <DD> Marks a node as not visited

 <DT> <A HREF="dddmpAllDet.html#NumberNodeRecurCnf" TARGET="MAIN"><CODE>NumberNodeRecurCnf()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCheckIncomingAndScanPath" TARGET="MAIN"><CODE>DddmpDdNodesCheckIncomingAndScanPath()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesNumberEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesNumberEdgesRecur()</CODE></A>
 <DD> Number nodes recursively in post-order

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesResetCountRecur" TARGET="MAIN"><CODE>DddmpDdNodesResetCountRecur()</CODE></A>
 <DD> Resets counter and visited flag for ALL nodes of a BDD

 <DT> <A HREF="dddmpAllDet.html#DddmpDdNodesCountEdgesRecur" TARGET="MAIN"><CODE>DddmpDdNodesCountEdgesRecur()</CODE></A>
 <DD> Counts the number of incoming edges for each node of a BDD

 <DT> <A HREF="dddmpAllDet.html#RemoveFromUniqueRecurCnf" TARGET="MAIN"><CODE>RemoveFromUniqueRecurCnf()</CODE></A>
 <DD> Removes a node from unique table

 <DT> <A HREF="dddmpAllDet.html#RestoreInUniqueRecurCnf" TARGET="MAIN"><CODE>RestoreInUniqueRecurCnf()</CODE></A>
 <DD> Restores a node in unique table

 <DT> <A HREF="dddmpAllDet.html#DddmpPrintBddAndNextRecur" TARGET="MAIN"><CODE>DddmpPrintBddAndNextRecur()</CODE></A>
 <DD> Prints debug info

</DL>
<HR>
<A NAME="dddmpStoreAdd.c"><H1>dddmpStoreAdd.c</H1></A>
Functions to write ADDs to file. <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to write ADDs to file.
    ADDs are represended on file either in text or binary format under the
    following rules.  A file contains a forest of ADDs (a vector of
    Boolean functions).  ADD nodes are numbered with contiguous numbers,
    from 1 to NNodes (total number of nodes on a file). 0 is not used to
    allow negative node indexes for complemented edges.  A file contains
    a header, including information about variables and roots to ADD
    functions, followed by the list of nodes.
    ADD nodes are listed according to their numbering, and in the present
    implementation numbering follows a post-order strategy, in such a way
    that a node is never listed before its Then/Else children. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddStore" TARGET="MAIN"><CODE>Dddmp_cuddAddStore()</CODE></A>
 <DD> Writes a dump file representing the argument ADD.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddAddArrayStore" TARGET="MAIN"><CODE>Dddmp_cuddAddArrayStore()</CODE></A>
 <DD> Writes a dump file representing the argument Array of ADDs.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBdd" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBdd()</CODE></A>
 <DD> Writes a dump file representing the argument Array of
    BDDs/ADDs.

 <DT> <A HREF="dddmpAllDet.html#NodeStoreRecurAdd" TARGET="MAIN"><CODE>NodeStoreRecurAdd()</CODE></A>
 <DD> Performs the recursive step of Dddmp_bddStore.

 <DT> <A HREF="dddmpAllDet.html#NodeTextStoreAdd" TARGET="MAIN"><CODE>NodeTextStoreAdd()</CODE></A>
 <DD> Store One Single Node in Text Format.

</DL>
<HR>
<A NAME="dddmpStoreBdd.c"><H1>dddmpStoreBdd.c</H1></A>
Functions to write BDDs to file. <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to write BDDs to file.
    BDDs are represended on file either in text or binary format under the
    following rules.  A file contains a forest of BDDs (a vector of
    Boolean functions).  BDD nodes are numbered with contiguous numbers,
    from 1 to NNodes (total number of nodes on a file). 0 is not used to
    allow negative node indexes for complemented edges.  A file contains
    a header, including information about variables and roots to BDD
    functions, followed by the list of nodes.  BDD nodes are listed
    according to their numbering, and in the present implementation
    numbering follows a post-order strategy, in such a way that a node
    is never listed before its Then/Else children. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStore" TARGET="MAIN"><CODE>Dddmp_cuddBddStore()</CODE></A>
 <DD> Writes a dump file representing the argument BDD.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStore" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStore()</CODE></A>
 <DD> Writes a dump file representing the argument Array of BDDs.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddBddArrayStore" TARGET="MAIN"><CODE>DddmpCuddBddArrayStore()</CODE></A>
 <DD> Writes a dump file representing the argument Array of
    BDDs.

 <DT> <A HREF="dddmpAllDet.html#NodeStoreRecurBdd" TARGET="MAIN"><CODE>NodeStoreRecurBdd()</CODE></A>
 <DD> Performs the recursive step of Dddmp_bddStore.

 <DT> <A HREF="dddmpAllDet.html#NodeTextStoreBdd" TARGET="MAIN"><CODE>NodeTextStoreBdd()</CODE></A>
 <DD> Store One Single Node in Text Format.

 <DT> <A HREF="dddmpAllDet.html#NodeBinaryStoreBdd" TARGET="MAIN"><CODE>NodeBinaryStoreBdd()</CODE></A>
 <DD> Store One Single Node in Binary Format.

</DL>
<HR>
<A NAME="dddmpStoreCnf.c"><H1>dddmpStoreCnf.c</H1></A>
Functions to write out BDDs to file in a CNF format <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to write out BDDs to file in a CNF format. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStoreCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddStoreCnf()</CODE></A>
 <DD> Writes a dump file representing the argument BDD in
    a CNF format.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStoreCnf" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStoreCnf()</CODE></A>
 <DD> Writes a dump file representing the argument array of BDDs
    in CNF format.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddBddArrayStoreCnf" TARGET="MAIN"><CODE>DddmpCuddBddArrayStoreCnf()</CODE></A>
 <DD> Writes a dump file representing the argument Array of
    BDDs in the CNF standard format.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfNodeByNode" TARGET="MAIN"><CODE>StoreCnfNodeByNode()</CODE></A>
 <DD> Store the BDD as CNF clauses.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfNodeByNodeRecur" TARGET="MAIN"><CODE>StoreCnfNodeByNodeRecur()</CODE></A>
 <DD> Performs the recursive step of Dddmp_bddStore.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfOneNode" TARGET="MAIN"><CODE>StoreCnfOneNode()</CODE></A>
 <DD> Store One Single BDD Node.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfMaxtermByMaxterm" TARGET="MAIN"><CODE>StoreCnfMaxtermByMaxterm()</CODE></A>
 <DD> Prints a disjoint sum of products.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfBest" TARGET="MAIN"><CODE>StoreCnfBest()</CODE></A>
 <DD> Prints a disjoint sum of products with intermediate
    cutting points.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfMaxtermByMaxtermRecur" TARGET="MAIN"><CODE>StoreCnfMaxtermByMaxtermRecur()</CODE></A>
 <DD> Performs the recursive step of Print Maxterm.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfBestNotSharedRecur" TARGET="MAIN"><CODE>StoreCnfBestNotSharedRecur()</CODE></A>
 <DD> Performs the recursive step of Print Best on Not Shared
    sub-BDDs.

 <DT> <A HREF="dddmpAllDet.html#StoreCnfBestSharedRecur" TARGET="MAIN"><CODE>StoreCnfBestSharedRecur()</CODE></A>
 <DD> Performs the recursive step of Print Best on Shared
    sub-BDDs.

 <DT> <A HREF="dddmpAllDet.html#printCubeCnf" TARGET="MAIN"><CODE>printCubeCnf()</CODE></A>
 <DD> Print One Cube in CNF Format.

</DL>
<HR>
<A NAME="dddmpStoreMisc.c"><H1>dddmpStoreMisc.c</H1></A>
Functions to write out bdds to file in prefixed
    and in Blif form. <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to write out bdds to file. 
    BDDs are represended on file in text format.
    Each node is stored as a multiplexer in a prefix notation format for
    the prefix notation file or in PLA format for the blif file. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStorePrefix" TARGET="MAIN"><CODE>Dddmp_cuddBddStorePrefix()</CODE></A>
 <DD> Writes a dump file representing the argument BDD in
    a prefix notation.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStorePrefix" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStorePrefix()</CODE></A>
 <DD> Writes a dump file representing the argument BDD in
    a prefix notation.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStoreBlif" TARGET="MAIN"><CODE>Dddmp_cuddBddStoreBlif()</CODE></A>
 <DD> Writes a dump file representing the argument BDD in
    a Blif/Exlif notation.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStoreBlif" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStoreBlif()</CODE></A>
 <DD> Writes a dump file representing the argument BDD in
    a Blif/Exlif notation.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddStoreSmv" TARGET="MAIN"><CODE>Dddmp_cuddBddStoreSmv()</CODE></A>
 <DD> Writes a dump file representing the argument BDD in
    a prefix notation.

 <DT> <A HREF="dddmpAllDet.html#Dddmp_cuddBddArrayStoreSmv" TARGET="MAIN"><CODE>Dddmp_cuddBddArrayStoreSmv()</CODE></A>
 <DD> Writes a dump file representing the argument BDD in
    a prefix notation.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStorePrefix" TARGET="MAIN"><CODE>DddmpCuddDdArrayStorePrefix()</CODE></A>
 <DD> Internal function to writes a dump file representing the
    argument BDD in a prefix notation.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStorePrefixBody" TARGET="MAIN"><CODE>DddmpCuddDdArrayStorePrefixBody()</CODE></A>
 <DD> Internal function to writes a dump file representing the
    argument BDD in a prefix notation. Writes the body of the file.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStorePrefixStep" TARGET="MAIN"><CODE>DddmpCuddDdArrayStorePrefixStep()</CODE></A>
 <DD> Performs the recursive step of
    DddmpCuddDdArrayStorePrefixBody.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBlif" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBlif()</CODE></A>
 <DD> Writes a blif file representing the argument BDDs.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBlifBody" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBlifBody()</CODE></A>
 <DD> Writes a blif body representing the argument BDDs.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreBlifStep" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreBlifStep()</CODE></A>
 <DD> Performs the recursive step of DddmpCuddDdArrayStoreBlif.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreSmv" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreSmv()</CODE></A>
 <DD> Internal function to writes a dump file representing the
    argument BDD in a SMV notation.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreSmvBody" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreSmvBody()</CODE></A>
 <DD> Internal function to writes a dump file representing the
    argument BDD in a SMV notation. Writes the body of the file.

 <DT> <A HREF="dddmpAllDet.html#DddmpCuddDdArrayStoreSmvStep" TARGET="MAIN"><CODE>DddmpCuddDdArrayStoreSmvStep()</CODE></A>
 <DD> Performs the recursive step of
    DddmpCuddDdArrayStoreSmvBody.

</DL>
<HR>
<A NAME="dddmpUtil.c"><H1>dddmpUtil.c</H1></A>
Util Functions for the dddmp package <P>
<B>By: Gianpiero Cabodi and Stefano Quer</B><P>
Functions to manipulate arrays. <P>
<DL>
 <DT> <A HREF="dddmpAllDet.html#QsortStrcmp" TARGET="MAIN"><CODE>QsortStrcmp()</CODE></A>
 <DD> String compare for qsort

 <DT> <A HREF="dddmpAllDet.html#FindVarname" TARGET="MAIN"><CODE>FindVarname()</CODE></A>
 <DD> Performs binary search of a name within a sorted array

 <DT> <A HREF="dddmpAllDet.html#DddmpStrDup" TARGET="MAIN"><CODE>DddmpStrDup()</CODE></A>
 <DD> Duplicates a string

 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayDup" TARGET="MAIN"><CODE>DddmpStrArrayDup()</CODE></A>
 <DD> Duplicates an array of strings

 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayRead" TARGET="MAIN"><CODE>DddmpStrArrayRead()</CODE></A>
 <DD> Inputs an array of strings

 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayWrite" TARGET="MAIN"><CODE>DddmpStrArrayWrite()</CODE></A>
 <DD> Outputs an array of strings

 <DT> <A HREF="dddmpAllDet.html#DddmpStrArrayFree" TARGET="MAIN"><CODE>DddmpStrArrayFree()</CODE></A>
 <DD> Frees an array of strings

 <DT> <A HREF="dddmpAllDet.html#DddmpIntArrayDup" TARGET="MAIN"><CODE>DddmpIntArrayDup()</CODE></A>
 <DD> Duplicates an array of ints

 <DT> <A HREF="dddmpAllDet.html#DddmpIntArrayRead" TARGET="MAIN"><CODE>DddmpIntArrayRead()</CODE></A>
 <DD> Inputs an array of ints

 <DT> <A HREF="dddmpAllDet.html#DddmpIntArrayWrite" TARGET="MAIN"><CODE>DddmpIntArrayWrite()</CODE></A>
 <DD> Outputs an array of ints

</DL>
<HR>
Last updated on 1040218 17h14
</BODY></HTML>
